Computer-aided verification in mechanism design

摘要

In mechanism design, the gold standard solution concepts are dominantstrategy incentive compatibility and Bayesian incentive compatibility. Thesesolution concepts relieve the (possibly unsophisticated) bidders from the needto engage in complicated strategizing. While incentive properties are simple tostate, their proofs are specific to the mechanism and can be quite complex.This raises two concerns. From a practical perspective, checking a complexproof can be a tedious process, often requiring experts knowledgeable inmechanism design. Furthermore, from a modeling perspective, if unsophisticatedagents are unconvinced of incentive properties, they may strategize inunpredictable ways. To address both concerns, we explore techniques from computer-aidedverification to construct formal proofs of incentive properties. Because formalproofs can be automatically checked, agents do not need to manually check theproperties, or even understand the proof. To demonstrate, we present theverification of a sophisticated mechanism: the generic reduction from Bayesianincentive compatible mechanism design to algorithm design given by Hartline,Kleinberg, and Malekian. This mechanism presents new challenges for formalverification, including essential use of randomness from both the execution ofthe mechanism and from the prior type distributions. As an immediateconsequence, our work also formalizes Bayesian incentive compatibility for theentire family of mechanisms derived via this reduction. Finally, as anintermediate step in our formalization, we provide the first formalverification of incentive compatibility for the celebratedVickrey-Clarke-Groves mechanism.